Nuprl Definition : bilinear_p 13,42
basic
IsBilinear(A;B;C;+a;+b;+c;f)
== (a1, a2:A, b:B. ((a1 +a a2) f b) = ((a1 f b) +c (a2 f b)))
== & (a:A, b1, b2:B. (a f (b1 +b b2)) = ((a f b1) +c (a f b2))) 
latex

clarification:

basic
IsBilinear(A;B;C;+a;+b;+c;f)
== (a1:A, a2:A, b:B. ((a1 +a a2) f b) = ((a1 f b) +c (a2 f b))  C)
== & (a:A. b1:B, b2:B. (a f (b1 +b b2)) = ((a f b1) +c (a f b2))  C) 
latex

Upgen algebra 1
Wellformedness Lemmasbilinear p wf
DefinitionsP & Q, x:A. B(x), x f y

origin